Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	not(not(x))	→ x
2:	not(or(x,y))	→ and(not(not(not(x))),not(not(not(y))))
3:	not(and(x,y))	→ or(not(not(not(x))),not(not(not(y))))

There are 12 dependency pairs:


4:	NOT(or(x,y))	→ NOT(not(not(x)))
5:	NOT(or(x,y))	→ NOT(not(x))
6:	NOT(or(x,y))	→ NOT(x)
7:	NOT(or(x,y))	→ NOT(not(not(y)))
8:	NOT(or(x,y))	→ NOT(not(y))
9:	NOT(or(x,y))	→ NOT(y)
10:	NOT(and(x,y))	→ NOT(not(not(x)))
11:	NOT(and(x,y))	→ NOT(not(x))
12:	NOT(and(x,y))	→ NOT(x)
13:	NOT(and(x,y))	→ NOT(not(not(y)))
14:	NOT(and(x,y))	→ NOT(not(y))
15:	NOT(and(x,y))	→ NOT(y)

Consider the SCC {4-15}. By taking the AF π with π(not) = π(NOT) = 1 together with the lexicographic path order with precedence and ≈ or, the rules in {1-3} are weakly decreasing and the rules in {4-15} are strictly decreasing. Hence the TRS is terminating.

Tyrolean Termination Tool (0.07 seconds) --- May 4, 2006